# hybrid_verification.py

import sys
from pathlib import Path
from importlib import import_module
import json
import os
import subprocess
from datetime import datetime
import argparse

def run_hybrid_verification():
    # 添加模块搜索路径 
    sys.path.insert(0, str(Path(__file__).parent / "formal/scripts"))
    sys.path.insert(0, str(Path(__file__).parent / "sim"))
    
    # 动态导入模块
    try:
        formal_module = import_module("formal_toolkit")
        sim_module = import_module("sim_module")
    except ImportError as e:
        print(f"模块导入错误: {e}")
        return
    # 获取项目根目录的绝对路径
    base_dir = Path(__file__).resolve().parent
    # 初始化配置
    wave_dir = str(base_dir / "results/waveforms")
    os.makedirs(wave_dir, exist_ok=True)
    
    # 运行形式验证
    print("运行形式验证...")
    formal_results = run_formal_verification(formal_module)
    
    if not formal_results:
        print("形式验证失败，终止流程")
        return
    
    # 准备仿真测试配置
    test_targets = formal_results.get("uncovered_areas", [])
    print(f"从形式验证中获取的测试目标: {test_targets}")
    
    timestamp = datetime.now().strftime("%Y%m%d_%H%M%S")
    sim_config = {
        "targets": test_targets,
        "duration": 200,  # 仿真周期数
        "clock_period": 20,  # ns
        "wave_path": str(Path("waveforms") / f"sim_{timestamp}.vcd"),
        "log_path": str(Path("logs") / f"sim_log_{timestamp}.log"),
    }
    
    # 运行仿真
    print("运行仿真验证...")
    sim_results = sim_module.run_simulation(sim_config)
    
    # 合并结果
    merged_results = merge_results(formal_results, sim_results)
    
    # 生成最终报告
    generate_final_report(merged_results)
    
    print("混合验证完成")

def run_formal_verification(formal_module):
    """运行形式验证工具"""
    try:
        FormalToolkitClass = formal_module.FormalToolkit
        formal_tool = FormalToolkitClass(cover_mode = True)
        
        sby_path = formal_tool.generate_sby_config()
        results = formal_tool.run_formal(sby_path)
        
        # 添加未覆盖区域信息
        # results["uncovered_areas"] = formal_tool._parse_uncovered_areas()
        
        return results
    except Exception as e:
        print(f"形式验证错误: {e}")
        return None

def merge_results(formal_results, sim_results):
    """合并形式验证和仿真结果"""
    # 合并覆盖率
    coverage = {
        "formal": formal_results.get("coverage", {}),
        "simulation": sim_results.get("coverage", {}),
        "combined": {}
    }
    
    # 简单的覆盖率合并策略：取最大值
    for key in set(formal_results["coverage"]) | set(sim_results["coverage"]):
        coverage["combined"][key] = max(
            formal_results["coverage"].get(key, 0),
            sim_results["coverage"].get(key, 0)
        )
    
    # 合并断言结果
    assertions = {
        "formal": formal_results.get("assertions", {}),
        "simulation": sim_results.get("assertions", {}),
        "status": "PASS"
    }
    
    # 检查是否有失败的断言
    for assert_type in assertions["formal"], assertions["simulation"]:
        for result in assert_type.values():
            if result != "PASS":
                assertions["status"] = "FAIL"
    
    return {
        "coverage": coverage,
        "assertions": assertions,
        "waveforms": {
            "formal": formal_results.get("traces", []),
            "simulation": sim_results.get("waveform_path")
        },
        "logs": {
            "formal": formal_results.get("log", ""),
            "simulation": sim_results.get("log", [])
        },
        "verification_status": "PASS" if coverage["combined"].get("overall", 0) > 95 and assertions["status"] == "PASS" else "FAIL"
    }

def generate_final_report(results):
    """生成最终验证报告"""
    report = {
        "title": "混合验证报告",
        "timestamp": datetime.now().isoformat(),
        "results": results
    }
    
    report_path = Path("results") / f"hybrid_report_{datetime.now().strftime('%Y%m%d_%H%M%S')}.json"
    report_path.parent.mkdir(exist_ok=True)
    
    with open(report_path, "w") as f:
        json.dump(report, f, indent=2)
    
    print(f"验证报告已生成: {report_path}")
    return report_path

if __name__ == "__main__":
    parser = argparse.ArgumentParser(description="混合验证框架")
    parser.add_argument("--formal-only", action="store_true", help="仅运行形式验证")
    parser.add_argument("--sim-only", action="store_true", help="仅运行仿真")
    args = parser.parse_args()
    
    if args.formal_only:
        # 仅运行形式验证
        pass
    elif args.sim_only:
        # 仅运行仿真
        pass
    else:
        run_hybrid_verification()